(set-logic ALL)
(set-option :model_validate true)
(set-option :model true)
(set-option :smt.arith.solver 4)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const r0 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(assert (= v4 (< i2 i2) v4 v1 v4 (< i2 i2)))
(declare-sort S0 0)
(declare-const bv_14-0 (_ BitVec 14))
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const r9 Real)
(assert v7)
(declare-const S0-0 S0)
(assert (not v1))
(declare-const i4 Int)
(declare-const S0-1 S0)
(declare-const bv_18-0 (_ BitVec 18))
(assert (<= 14117.811 r6 0.0))
(assert (> 51605.0 (/ r6 8.4853719) r4))
(check-sat)
(exit)